
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module ErgoSpec.Common.Utils.Result</title>
<meta name="description" content="Documentation of Coq module ErgoSpec.Common.Utils.Result" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>

<body onload="hideAll('proofscript')">
<h1 class="title">Module ErgoSpec.Common.Utils.Result</h1>
<div class="coq">
<br/>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.Ascii.html">Ascii</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html">String</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html">List</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.ZArith.ZArith.html">ZArith</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html">ErgoSpec.Backend.ErgoBackend</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html">ErgoSpec.Common.Utils.Provenance</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html">ErgoSpec.Common.Utils.Names</a></span>.<br/>
<br/>
<span class="kwd">Section</span> <span class="id"><a name="Result">Result</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Inductive</span> <span class="id"><a name="eerror">eerror</a></span> : <span class="kwd">Set</span> :=<br/>
&nbsp;&nbsp;| <span class="id"><a name="ESystemError">ESystemError</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eerror">eerror</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="EParseError">EParseError</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eerror">eerror</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="ECompilationError">ECompilationError</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eerror">eerror</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="ETypeError">ETypeError</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eerror">eerror</a></span><br/>
&nbsp;&nbsp;| <span class="id"><a name="ERuntimeError">ERuntimeError</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eerror">eerror</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="eresult">eresult</a></span> (<span class="id">A</span>:<span class="kwd">Set</span>) := <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Result">Result</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eerror">eerror</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="esuccess">esuccess</a></span> {<span class="id">A</span>:<span class="kwd">Set</span>} (<span class="id">a</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Success">Success</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eerror">eerror</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#a">a</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="efailure">efailure</a></span> {<span class="id">A</span>:<span class="kwd">Set</span>} (<span class="id">e</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eerror">eerror</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Failure">Failure</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eerror">eerror</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#e">e</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="Result.Lift">Lift</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="eolift">eolift</a></span> {<span class="id">A</span> <span class="id">B</span>:<span class="kwd">Set</span>} (<span class="id">f</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span>) (<span class="id">a</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#lift_failure">lift_failure</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#f">f</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#a">a</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="elift">elift</a></span> {<span class="id">A</span> <span class="id">B</span>:<span class="kwd">Set</span>} (<span class="id">f</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span>) (<span class="id">a</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#lift_failure_in">lift_failure_in</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#f">f</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#a">a</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="elift2">elift2</a></span> {<span class="id">A</span> <span class="id">B</span> <span class="id">C</span>:<span class="kwd">Set</span>} (<span class="id">f</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span>) (<span class="id">a</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) (<span class="id">b</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#lift_failure_in_two">lift_failure_in_two</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#f">f</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#a">a</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#b">b</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="elift3">elift3</a></span> {<span class="id">A</span> <span class="id">B</span> <span class="id">C</span> <span class="id">D</span>:<span class="kwd">Set</span>} (<span class="id">f</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#D">D</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">a</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) (<span class="id">b</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span>) (<span class="id">c</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#D">D</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#lift_failure_in_three">lift_failure_in_three</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#f">f</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#a">a</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#b">b</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#c">c</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="elift4">elift4</a></span> {<span class="id">A</span> <span class="id">B</span> <span class="id">C</span> <span class="id">D</span> <span class="id">E</span>:<span class="kwd">Set</span>} (<span class="id">f</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#D">D</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#E">E</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">a</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) (<span class="id">b</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span>) (<span class="id">c</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span>) (<span class="id">d</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#D">D</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#E">E</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span> (<span class="kwd">fun</span> <span class="id">x</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">g</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#g">g</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#x">x</a></span>) (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift3">elift3</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#f">f</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#a">a</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#b">b</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#c">c</a></span>)) <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#d">d</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="elift5">elift5</a></span> {<span class="id">A</span> <span class="id">B</span> <span class="id">C</span> <span class="id">D</span> <span class="id">E</span> <span class="id">F</span>:<span class="kwd">Set</span>} (<span class="id">f</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#D">D</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#E">E</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#F">F</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">a</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) (<span class="id">b</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span>) (<span class="id">c</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span>) (<span class="id">d</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#D">D</a></span>) (<span class="id">e</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#E">E</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#F">F</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span> (<span class="kwd">fun</span> <span class="id">x</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">g</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#g">g</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#x">x</a></span>) (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift4">elift4</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#f">f</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#a">a</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#b">b</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#c">c</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#d">d</a></span>)) <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#e">e</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="emaplift">emaplift</a></span> {<span class="id">A</span> <span class="id">B</span>:<span class="kwd">Set</span>} (<span class="id">f</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span>) (<span class="id">al</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#lift_failure_map">lift_failure_map</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#f">f</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#al">al</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="eresult_of_option">eresult_of_option</a></span> {<span class="id">A</span>:<span class="kwd">Set</span>} (<span class="id">a</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) (<span class="id">e</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eerror">eerror</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#result_of_option">result_of_option</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#a">a</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#e">e</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="elift_both">elift_both</a></span> {<span class="id">A</span> <span class="id">B</span>:<span class="kwd">Set</span>} (<span class="id">f</span>: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span>) (<span class="id">g</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eerror">eerror</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span>) (<span class="id">a</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#a">a</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Success">Success</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">s</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#f">f</a></span> <span class="id">s</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Failure">Failure</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">e</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#g">g</a></span> <span class="id">e</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="elift2_both">elift2_both</a></span> {<span class="id">A</span> <span class="id">B</span> <span class="id">C</span>:<span class="kwd">Set</span>} (<span class="id">f</span>: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span>) (<span class="id">g</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eerror">eerror</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span>) (<span class="id">a</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) (<span class="id">b</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#a">a</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Success">Success</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">s1</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#b">b</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Success">Success</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">s2</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#f">f</a></span> <span class="id">s1</span> <span class="id">s2</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Failure">Failure</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">e</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#g">g</a></span> <span class="id">e</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Failure">Failure</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">e</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#g">g</a></span> <span class="id">e</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="elift_maybe">elift_maybe</a></span> {<span class="id">A</span>:<span class="kwd">Set</span>} (<span class="id">f</span>: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>)) (<span class="id">a</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#f">f</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#a">a</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Success">Success</a></span> <span class="id">_</span> <span class="id">_</span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">s</span>) =&gt; <span class="id">s</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Success">Success</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#a">a</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Failure">Failure</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">e</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> <span class="id">e</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="eolift2">eolift2</a></span> {<span class="id">A</span> <span class="id">B</span> <span class="id">C</span>:<span class="kwd">Set</span>} (<span class="id">f</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span>) (<span class="id">a</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) (<span class="id">b</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift2">elift2</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#f">f</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#a">a</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#b">b</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Failure">Failure</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">f</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#f">f</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Success">Success</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">s</span> =&gt; <span class="id">s</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="elift_fold_left">elift_fold_left</a></span> {<span class="id">A</span>:<span class="kwd">Set</span>} {<span class="id">B</span>:<span class="kwd">Set</span>}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">f</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) (<span class="id">l</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span>) (<span class="id">a</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">proc_one</span> (<span class="id">acc</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) (<span class="id">x</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span> (<span class="kwd">fun</span> <span class="id">acc</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#f">f</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#acc">acc</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#x">x</a></span>) <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#acc">acc</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_left">fold_left</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#proc_one">proc_one</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#l">l</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#a">a</a></span>).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="elift_context_fold_left_alt">elift_context_fold_left_alt</a></span> {<span class="id">A</span>:<span class="kwd">Set</span>} {<span class="id">B</span>:<span class="kwd">Set</span>} {<span class="id">C</span>:<span class="kwd">Set</span>}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">f</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span> * <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span>)) (<span class="id">l</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) (<span class="id">c</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span> * <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift_fold_left">elift_fold_left</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">acc</span> <span class="id">c</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">mc</span> =&gt; ((<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#acc">acc</a></span>)++((<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#mc">mc</a></span>)::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>), <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#mc">mc</a></span>)) (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#f">f</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#acc">acc</a></span>) <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#c">c</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#l">l</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#c">c</a></span>).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="elift_context_fold_left">elift_context_fold_left</a></span> {<span class="id">A</span>:<span class="kwd">Set</span>} {<span class="id">B</span>:<span class="kwd">Set</span>} {<span class="id">C</span>:<span class="kwd">Set</span>}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">f</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span> * <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span>)) (<span class="id">l</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) (<span class="id">c</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span> * <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#C">C</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift_fold_left">elift_fold_left</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">acc</span> <span class="id">c</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">mc</span> =&gt; ((<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#acc">acc</a></span>)++((<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#mc">mc</a></span>)::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>), <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#mc">mc</a></span>)) (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#f">f</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#acc">acc</a></span>) <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#c">c</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#l">l</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#c">c</a></span>).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="eflatmaplift">eflatmaplift</a></span> {<span class="id">A</span> <span class="id">B</span>:<span class="kwd">Set</span>} (<span class="id">f</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> -&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span>)) (<span class="id">al</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#B">B</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift_fold_left">elift_fold_left</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">acc</span> <span class="id">c</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span> (<span class="kwd">fun</span> <span class="id">mc</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#acc">acc</a></span> ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#mc">mc</a></span>) (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#f">f</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#c">c</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#al">al</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="Result.Lift.qcert">qcert</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="eerror_of_qerror">eerror_of_qerror</a></span> (<span class="id">prov</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span>) (<span class="id">qe</span>:<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Results.QResult.html#qerror">qerror</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#qe">qe</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Results.QResult.html#CompilationError">QResult.CompilationError</a></span> <span class="id">msg</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> <span class="id">msg</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Results.QResult.html#TypeError">QResult.TypeError</a></span> <span class="id">msg</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ETypeError">ETypeError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> <span class="id">msg</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Results.QResult.html#UserError">QResult.UserError</a></span> <span class="id">msg</span> =&gt;  <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ESystemError">ESystemError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "<span class="id">User</span> <span class="id">error</span> <span class="id">occured</span> <span class="kwd">in</span> <span class="id">backend</span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="eresult_of_qresult">eresult_of_qresult</a></span> {<span class="id">A</span>:<span class="kwd">Set</span>} (<span class="id">prov</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span>) (<span class="id">a</span>:<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Results.QResult.html#qresult">qresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#a">a</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Success">Result.Success</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">s</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#esuccess">esuccess</a></span> <span class="id">s</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Failure">Result.Failure</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">e</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eerror_of_qerror">eerror_of_qerror</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> <span class="id">e</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="option_of_eresult">option_of_eresult</a></span> {<span class="id">A</span>:<span class="kwd">Set</span>} (<span class="id">a</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#option_of_result">option_of_result</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#a">a</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#Result.Lift.qcert">qcert</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#Result.Lift">Lift</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="Result.Fmt">Fmt</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="format_error">format_error</a></span> (<span class="id">name</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) (<span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span>) (<span class="id">msg</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">loc</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#loc_of_provenance">loc_of_provenance</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#name">name</a></span> ++ " <span class="tactic">at</span> " ++ (<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#string_of_location">string_of_location</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#loc">loc</a></span>) ++ " '" ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#msg">msg</a></span> ++ "'")%<span class="id">string</span>.<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#Result.Fmt">Fmt</a></span>.<br/>
&nbsp;&nbsp;<br/>
<div class="doc">Built-in errors </div>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="Result.Builtin">Builtin</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="clause_call_not_on_contract_error">clause_call_not_on_contract_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "<span class="id">Cannot</span> <span class="id">call</span> <span class="id">a</span> <span class="id">clause</span> <span class="id">except</span> <span class="id">on</span> '<span class="id">contract</span>'").<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="use_contract_not_in_contract_error">use_contract_not_in_contract_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "<span class="id">Cannot</span> <span class="id">use</span> '<span class="id">contract</span>' <span class="id">variable</span> <span class="id">outside</span> <span class="id">of</span> <span class="id">a</span> <span class="id">contract</span>").<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="call_clause_not_in_contract_error">call_clause_not_in_contract_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> <span class="id">clname</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="id">Cannot</span> <span class="id">call</span> <span class="id">clause</span> " ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#clname">clname</a></span> ++ " <span class="id">outside</span> <span class="id">of</span> <span class="id">a</span> <span class="id">contract</span>")).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="not_in_clause_error">not_in_clause_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "<span class="id">Cannot</span> <span class="id">use</span> '<span class="id">clause</span>' <span class="id">variable</span> <span class="id">outside</span> <span class="id">of</span> <span class="id">a</span> <span class="id">clause</span>").<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="import_not_found_error">import_not_found_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> (<span class="id">import</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="kwd">Import</span> <span class="id">not</span> <span class="id">found</span>: " ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#import">import</a></span>)).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="type_name_not_found_error">type_name_not_found_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> (<span class="id">ln</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="id">Cannot</span> <span class="id">find</span> <span class="id">type</span> <span class="kwd">with</span> <span class="id">name</span> '" ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ln">ln</a></span> ++ "'")).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="variable_name_not_found_error">variable_name_not_found_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> (<span class="id">ln</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="id">Cannot</span> <span class="id">find</span> <span class="id">variable</span> <span class="kwd">with</span> <span class="id">name</span> '" ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ln">ln</a></span> ++ "'")).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="function_name_not_found_error">function_name_not_found_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> (<span class="id">ln</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="id">Cannot</span> <span class="id">find</span> <span class="id">function</span> <span class="kwd">with</span> <span class="id">name</span> '" ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ln">ln</a></span> ++ "'")).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="contract_name_not_found_error">contract_name_not_found_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> (<span class="id">ln</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="id">Cannot</span> <span class="id">find</span> <span class="id">contract</span> <span class="kwd">with</span> <span class="id">name</span> '" ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ln">ln</a></span> ++ "'")).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="import_name_not_found_error">import_name_not_found_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> (<span class="id">namespace</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) (<span class="id">name_ref</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="id">Cannot</span> <span class="id">import</span> <span class="id">name</span> '" ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#name_ref">name_ref</a></span>++ "' <span class="kwd">in</span> <span class="id">CTO</span> <span class="kwd">with</span> <span class="id">namespace</span> " ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#namespace">namespace</a></span>)).<br/>
&nbsp;&nbsp;<br/>
<div class="doc">Main clause creation errors </div>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="main_parameter_mismatch_error">main_parameter_mismatch_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "<span class="kwd">Parameter</span> <span class="id">mismatch</span> <span class="id">during</span> <span class="id">main</span> <span class="id">creation</span>").<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="main_at_least_one_parameter_error">main_at_least_one_parameter_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "<span class="id">Cannot</span> <span class="id">create</span> <span class="id">main</span> <span class="kwd">if</span> <span class="id">not</span> <span class="tactic">at</span> <span class="id">least</span> <span class="id">one</span> <span class="id">parameter</span>").<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="main_not_a_class_error">main_not_a_class_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> (<span class="id">cname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="id">Cannot</span> <span class="id">create</span> <span class="id">main</span> <span class="kwd">for</span> <span class="id">non</span>-<span class="id">class</span> <span class="id">type</span> "++<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#cname">cname</a></span>)).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
<div class="doc">Call errors </div>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="function_not_found_error">function_not_found_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> (<span class="id">fname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="id">Function</span> '" ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#fname">fname</a></span> ++ "' <span class="id">not</span> <span class="id">found</span>")).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="eval_function_not_found_error">eval_function_not_found_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> (<span class="id">fname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ERuntimeError">ERuntimeError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="id">Function</span> '" ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#fname">fname</a></span> ++ "' <span class="id">not</span> <span class="id">found</span> <span class="id">during</span> <span class="id">eval</span>")).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="clause_not_found_error">clause_not_found_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> (<span class="id">fname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="id">Clause</span> '" ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#fname">fname</a></span> ++ "' <span class="id">not</span> <span class="id">found</span>")).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="call_params_error">call_params_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> (<span class="id">fname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="kwd">Parameter</span> <span class="id">mismatch</span> <span class="id">when</span> <span class="id">calling</span> <span class="id">function</span> '" ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#fname">fname</a></span> ++ "'")).<br/>
<br/>
<div class="doc">Other runtime errors </div>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="eval_unary_op_error">eval_unary_op_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> (<span class="id">op</span>:<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoOps.Unary.op">ErgoOps.Unary.op</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ERuntimeError">ERuntimeError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "<span class="id">Unary</span> <span class="id">operation</span> <span class="id">failed</span>.").<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="eval_binary_op_error">eval_binary_op_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> (<span class="id">op</span>:<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoOps.Binary.op">ErgoOps.Binary.op</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ERuntimeError">ERuntimeError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "<span class="id">Binary</span> <span class="id">operation</span> <span class="id">failed</span>.").<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="eval_if_not_boolean_error">eval_if_not_boolean_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ERuntimeError">ERuntimeError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "'<span class="id">If</span>' <span class="id">condition</span> <span class="id">not</span> <span class="id">boolean</span>.").<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="eval_match_let_optional_not_on_option_error">eval_match_let_optional_not_on_option_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ERuntimeError">ERuntimeError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "<span class="id">Matched</span> <span class="id">LetOption</span> <span class="id">without</span> <span class="id">an</span> <span class="id">option</span>.").<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="eval_foreach_not_on_array_error">eval_foreach_not_on_array_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ERuntimeError">ERuntimeError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "<span class="id">Foreach</span> <span class="id">needs</span> <span class="id">to</span> <span class="id">be</span> <span class="id">called</span> <span class="id">on</span> <span class="id">an</span> <span class="id">array</span>").<br/>
<br/>
<div class="doc">System errors </div>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="no_ergo_module_error">no_ergo_module_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ESystemError">ESystemError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="id">No</span> <span class="id">input</span> <span class="id">ergo</span> <span class="id">found</span>")).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="built_in_function_not_found_error">built_in_function_not_found_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> (<span class="id">fname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ESystemError">ESystemError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="id">Built</span> <span class="kwd">in</span> <span class="id">function</span> " ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#fname">fname</a></span> ++ " <span class="id">not</span> <span class="id">found</span>")).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="built_in_function_without_body_error">built_in_function_without_body_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> (<span class="id">fname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ESystemError">ESystemError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="id">Built</span> <span class="kwd">in</span> <span class="id">function</span> " ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#fname">fname</a></span> ++ " <span class="id">does</span> <span class="id">not</span> <span class="id">have</span> <span class="id">a</span> <span class="id">body</span>")).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="TODO">TODO</a></span> {<span class="id">A</span> : <span class="kwd">Set</span>} <span class="id">prov</span> (<span class="id">feature</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ESystemError">ESystemError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="id">Feature</span> " ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#feature">feature</a></span> ++ " <span class="id">not</span> <span class="id">implemented</span>.")%<span class="id">string</span>).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="enforce_error_content">enforce_error_content</a></span> (<span class="id">prov</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span>) (<span class="id">msg</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoData.data">ErgoData.data</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">message</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#format_error">format_error</a></span> "<span class="id">Enforce</span> <span class="id">Error</span>" <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#msg">msg</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoData.dbrand">ErgoData.dbrand</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#default_error_absolute_name">default_error_absolute_name</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoData.drec">ErgoData.drec</a></span> (("<span class="id">message</span>"%<span class="id">string</span>, <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoData.dstring">ErgoData.dstring</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#message">message</a></span>)::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="default_match_error_content">default_match_error_content</a></span> (<span class="id">prov</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#provenance">provenance</a></span>) (<span class="id">msg</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoData.data">ErgoData.data</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">message</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#format_error">format_error</a></span> "<span class="id">DefaultMatch</span> <span class="id">Error</span>" <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#msg">msg</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoData.dbrand">ErgoData.dbrand</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#default_error_absolute_name">default_error_absolute_name</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoData.drec">ErgoData.drec</a></span> (("<span class="id">message</span>"%<span class="id">string</span>, <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoData.dstring">ErgoData.dstring</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#message">message</a></span>)::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="unresolved_name_error">unresolved_name_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "<span class="id">Unresolved</span> <span class="id">name</span>").<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="should_have_one_contract_error">should_have_one_contract_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ECompilationError">ECompilationError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "<span class="id">Should</span> <span class="id">have</span> <span class="id">exactly</span> <span class="id">one</span> <span class="id">contract</span>").<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="contract_in_calculus_error">contract_in_calculus_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ESystemError">ESystemError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "<span class="id">Should</span> <span class="id">not</span> <span class="id">find</span> '<span class="id">contract</span>' <span class="kwd">in</span> <span class="id">Ergo</span> <span class="id">Calculus</span>").<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="clause_in_calculus_error">clause_in_calculus_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ESystemError">ESystemError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "<span class="id">Should</span> <span class="id">not</span> <span class="id">find</span> '<span class="id">clause</span>' <span class="kwd">in</span> <span class="id">Ergo</span> <span class="id">Calculus</span>").<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="state_in_calculus_error">state_in_calculus_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ESystemError">ESystemError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "<span class="id">Should</span> <span class="id">not</span> <span class="id">find</span> '<span class="id">state</span>' <span class="kwd">in</span> <span class="id">Ergo</span> <span class="id">Calculus</span>").<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="complex_foreach_in_calculus_error">complex_foreach_in_calculus_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ESystemError">ESystemError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> "<span class="id">Should</span> <span class="id">only</span> <span class="id">have</span> <span class="id">single</span> <span class="id">loop</span> <span class="id">foreach</span> <span class="kwd">in</span> <span class="id">Ergo</span> <span class="id">Calculus</span>").<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="function_not_inlined_error">function_not_inlined_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> <span class="id">fname</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ESystemError">ESystemError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="id">Function</span> " ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#fname">fname</a></span> ++ " <span class="id">did</span> <span class="id">not</span> <span class="id">get</span> <span class="id">inlined</span>")).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="function_in_group_not_inlined_error">function_in_group_not_inlined_error</a></span> {<span class="id">A</span>} <span class="id">prov</span> <span class="id">gname</span> <span class="id">fname</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#A">A</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#efailure">efailure</a></span> (<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#ESystemError">ESystemError</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#prov">prov</a></span> ("<span class="id">Clause</span> " ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#fname">fname</a></span> ++ " <span class="kwd">in</span> <span class="id">contract</span> " ++ <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#gname">gname</a></span> ++ " <span class="id">did</span> <span class="id">not</span> <span class="id">get</span> <span class="id">inlined</span>")).<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#Result.Builtin">Builtin</a></span>.<br/>
<br/>
<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#Result">Result</a></span>.<br/>

</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>
